GermanWikipedia - /page/entry.mu

Micron Document

<!DOCTYPE html>

<title>DPLL-Algorithmus</title>

</head>

<h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">DPLL-Algorithmus</span></h1>

</header>

</div>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="de" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="de" dir="ltr"><p>In der <a href="Logik" title="Logik">Logik</a> und <a href="Informatik" title="Informatik">Informatik</a> ist der <b>Davis-Putnam-Logemann-Loveland (DPLL)-Algorithmus</b> ein vollständiger, auf <a href="Backtracking" title="Backtracking">Backtracking</a> basierender Suchalgorithmus zur Bestimmung der Erfüllbarkeit von Formeln der <a href="Aussagenlogik" title="Aussagenlogik">Aussagenlogik</a> in <a href="Konjunktive_Normalform" title="Konjunktive Normalform">konjunktiver Normalform</a>, d. h. zur Lösung des CNF-SAT-Problems.

</p><p>Er wurde 1961 von <a href="Martin_Davis" title="Martin Davis">Martin Davis</a>, George Logemann und Donald W. Loveland eingeführt und ist eine Verfeinerung des früheren Davis-Putnam-Algorithmus, der ein von Davis und <a href="Hilary_Putnam" title="Hilary Putnam">Hilary Putnam</a> 1960 entwickeltes auflösungsbasiertes Verfahren ist. Vor allem in älteren Veröffentlichungen wird der Davis-Logemann-Loveland-Algorithmus oft als „Davis-Putnam-Methode“ oder „DP-Algorithmus“ bezeichnet. Andere gebräuchliche Bezeichnungen, die diese Unterscheidung beibehalten, sind DLL und DPLL.

</p>

<div class="mw-heading mw-heading2"><h2 id="Implementierungen_und_Anwendungen">Implementierungen und Anwendungen</h2></div>

<p>Das <a href="Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" title="Erfüllbarkeitsproblem der Aussagenlogik">SAT-Problem</a> ist sowohl aus theoretischer als auch aus praktischer Sicht von Bedeutung. In der <a href="Komplexit%C3%A4tstheorie" title="Komplexitätstheorie">Komplexitätstheorie</a> war es das erste Problem, das sich als <a href="NP-Vollst%C3%A4ndigkeit" title="NP-Vollständigkeit">NP-vollständig</a> erwiesen hat, und es kann in einer Vielzahl von Anwendungen vorkommen, z. B. bei der Modellprüfung, der automatischen Planung und Terminierung und der Diagnose in der <a href="K%C3%BCnstliche_Intelligenz" title="Künstliche Intelligenz">künstlichen Intelligenz</a>.

</p><p>Daher ist die Entwicklung effizienter SAT-Löser seit vielen Jahren ein Forschungsthema. GRASP (1996–1999) war eine frühe Implementierung unter Verwendung von DPLL.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Bei den internationalen SAT-Wettbewerben belegten Implementierungen auf der Grundlage von DPLL wie zChaff<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> und MiniSat<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> in den Jahren 2004 und 2005 die ersten Plätze.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup>

</p><p>Eine weitere Anwendung, bei der DPLL häufig zum Einsatz kommt, ist das automatisierte <a href="Maschinengest%C3%BCtztes_Beweisen" title="Maschinengestütztes Beweisen">Theorembeweisen</a> oder die Satisfiability Modulo Theories (SMT), ein <a href="Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" title="Erfüllbarkeitsproblem der Aussagenlogik">SAT-Problem</a>, bei dem propositionale Variablen durch Formeln einer anderen mathematischen Theorie ersetzt werden.

</p>

<div class="mw-heading mw-heading2"><h2 id="Der_Algorithmus">Der Algorithmus</h2></div>

<p>Der grundlegende Backtracking-Algorithmus läuft so ab, dass ein Literal ausgewählt, diesem ein Wahrheitswert zugewiesen, die Formel vereinfacht und dann rekursiv geprüft wird, ob die vereinfachte Formel erfüllbar ist. Ist dies der Fall, so ist die ursprüngliche Formel erfüllbar; andernfalls wird dieselbe rekursive Prüfung unter Annahme des entgegengesetzten Wahrheitswertes durchgeführt. Dies wird als Splitting-Regel bezeichnet, da sie das Problem in zwei einfachere Teilprobleme aufteilt. Durch den Vereinfachungsschritt werden im Wesentlichen alle Klauseln, die durch die Zuweisung wahr werden, aus der Formel entfernt, und alle Literale, die falsch werden, aus den verbleibenden Klauseln.

</p><p>Der DPLL-Algorithmus verbessert sich gegenüber dem Backtracking-Algorithmus durch die gezielte Anwendung der folgenden Regeln bei jedem Schritt:

</p><p><b>Weitergabe von Einheiten</b>

</p>

<ul><li>Wenn eine Klausel eine Einheitsklausel ist, d. h. sie enthält nur ein einziges nicht zugewiesenes Literal, kann diese Klausel nur durch Zuweisung des erforderlichen Wertes erfüllt werden, um dieses Literal wahr zu machen. Es ist also keine Auswahl erforderlich. Die Einheitspropagierung besteht darin, jede Klausel zu entfernen, die das Literal einer Einheitsklausel enthält, und das Komplement des Literales einer Einheitsklausel aus jeder Klausel zu verwerfen, die dieses Komplement enthält. In der Praxis führt dies oft zu deterministischen Kaskaden von Einheiten, wodurch ein großer Teil des naiven Suchraums vermieden wird.</li></ul>

<p><b>Reine Literaleliminierung</b>

</p>

<ul><li>Wenn eine Satzvariable nur mit einer Polarität in der Formel vorkommt, wird sie als rein bezeichnet. Ein reines Literal kann immer so zugewiesen werden, dass alle Klauseln, die es enthalten, wahr werden. Wenn es also auf diese Weise zugewiesen wird, schränken diese Klauseln die Suche nicht mehr ein und können gelöscht werden.</li></ul>

<p>Die Unerfüllbarkeit einer gegebenen Teilzuweisung wird festgestellt, wenn eine Klausel leer wird, d. h. wenn alle Variablen so zugewiesen wurden, dass die entsprechenden Literale falsch sind. Die Erfüllbarkeit der Formel wird entweder festgestellt, wenn alle Variablen zugewiesen werden, ohne dass die leere Klausel entsteht, oder, in modernen Implementierungen, wenn alle Klauseln erfüllt sind. Die Unerfüllbarkeit der vollständigen Formel kann nur nach einer erschöpfenden Suche festgestellt werden.

</p><p>Der DPLL-Algorithmus lässt sich in folgendem Pseudocode zusammenfassen, wobei Φ die CNF-Formel ist:

</p>

<pre> Eingabe: Eine Menge von Klauseln Φ.

Ausgabe: Ein Wahrheitswert, der angibt, ob Φ erfüllbar ist.

</pre>

<pre><b>Funktion</b> <i>DPLL</i>(Φ)

// Weitergabe von Einheiten:

<b>while</b> es gibt eine Einheitsklausel {<i>l</i>} in Φ <b>do</b>

Φ ← <i>unit-propagate</i>(<i>l</i>, Φ);

// reine Literaleliminierung:

<b>while</b> gibt es ein Literal <i>l</i>, das rein in Φ vorkommt <b>do</b>

Φ ← <i>pure-literal-assign</i>(<i>l</i>, Φ);

// Haltebedingungen:

<b>return</b> true;

<b>if</b> Φ eine leere Klausel enthält, <b>dann</b>

<b>return</b> false;

// DPLL-Prozedur:

<i>l</i> ← <i>choose-literal</i>(Φ);

<b>return</b> <i>DPLL</i>(Φ <b>∧</b> {l}) <b>or</b> <i>DPLL</i>(Φ <b>∧</b> {¬l});

</pre>

<p>In diesem Pseudocode sind unit-propagate(l, Φ) und pure-literal-assign(l, Φ) Funktionen, die das Ergebnis der Anwendung der unit-propagate- bzw. der pure-literal-Regel auf das Literal l und die Formel Φ zurückgeben. Mit anderen Worten: Sie ersetzen jedes Vorkommen von l durch „wahr“ und jedes Vorkommen von nicht l durch „falsch“ in der Formel Φ und vereinfachen die resultierende Formel. Das oder in der Return-Anweisung ist ein Kurzschlussoperator. Φ ∧ {l} bezeichnet das vereinfachte Ergebnis der Ersetzung von l durch „wahr“ in Φ.

</p><p>Der Algorithmus bricht in einem von zwei Fällen ab. Entweder ist die CNF-Formel Φ leer, d. h. sie enthält keine Klausel. Dann ist sie durch jede beliebige Zuweisung erfüllt, da alle ihre Klauseln leer wahr sind. Andernfalls, wenn die Formel eine leere Klausel enthält, ist die Klausel leer falsch, da eine Disjunktion mindestens ein wahres Glied erfordert, damit die Gesamtmenge wahr ist. In diesem Fall bedeutet das Vorhandensein einer solchen Klausel, dass die Formel (ausgewertet als Konjunktion aller Klauseln) nicht als wahr ausgewertet werden kann und nicht erfüllbar sein muss.

</p><p>Die Pseudocode-DPLL-Funktion gibt nur zurück, ob die endgültige Zuordnung die Formel erfüllt oder nicht. In einer realen Implementierung wird bei Erfolg typischerweise auch die teilerfüllende Zuweisung zurückgegeben; dies lässt sich aus der Verfolgung von verzweigenden Literalen und den Literalzuweisungen ableiten, die während der Einheitenfortpflanzung und der reinen Literaleliminierung vorgenommen werden.

</p><p>Der Davis-Logemann-Loveland-Algorithmus hängt von der Wahl des Verzweigungsliterales ab, d. h. des Literales, das im Backtracking-Schritt berücksichtigt wird. Folglich handelt es sich nicht um einen Algorithmus, sondern um eine Familie von Algorithmen, einen für jede mögliche Wahl des Verzweigungsliterales. Die Effizienz wird durch die Wahl des Verzweigungsliterales stark beeinflusst: Es gibt Fälle, bei denen die Laufzeit je nach Wahl des Verzweigungsliterales konstant oder exponentiell ist. Solche Wahlfunktionen werden auch als heuristische Funktionen oder Verzweigungsheuristiken bezeichnet[5].

</p>

<div class="mw-heading mw-heading3"><h3 id="Visualisierung">Visualisierung</h3></div>

<p>Davis, Logemann, Loveland (1961) hatten diesen Algorithmus entwickelt.

Einige Eigenschaften dieses ursprünglichen Algorithmus sind:

</p>

<ul><li>Er basiert auf der Suche.</li>

<li>Er ist die Grundlage für fast alle modernen SAT-Löser.</li>

<li>Er verwendet kein Lernen oder nicht-chronologisches Backtracking (eingeführt 1996).</li></ul>

<p>Ein Beispiel mit Visualisierung für einen DPLL-Algorithmus mit chronologischem Backtracking:

</p>

<div class="gallerytext">Alle Klauseln, die eine CNF-Formel bilden</div>

</li>

<div class="gallerytext">Wählen Sie eine Variable</div>

</li>

<div class="gallerytext">Entscheidung treffen, Variable a = Falsch (0), damit wird grüne Klausel Wahr</div>

</li>

<div class="gallerytext">Nachdem wir mehrere Entscheidungen getroffen haben, finden wir einen Implikationsgraph, der zu einem Konflikt führt.</div>

</li>

<div class="gallerytext">Nun kehren wir auf die unmittelbare Ebene zurück und weisen dieser Variablen zwangsweise den entgegengesetzten Wert zu</div>

</li>

<div class="gallerytext">Aber eine erzwungene Entscheidung führt immer noch zu einem weiteren Konflikt</div>

</li>

<div class="gallerytext">Zurück zur vorherigen Ebene gehen und eine erzwungene Entscheidung treffen</div>

</li>

<div class="gallerytext">Eine neue Entscheidung treffen, aber sie führt zu einem Konflikt</div>

</li>

<div class="gallerytext">Eine erzwungene Entscheidung treffen, aber sie führt wieder zu einem Konflikt</div>

</li>

<div class="gallerytext">Zurückgehen zum vorherigen Level</div>

</li>

<div class="gallerytext">Weiter so und der letzte Implikationsgraph</div>

</li>

</ul>

<div class="mw-heading mw-heading2"><h2 id="Verwandte_Algorithmen">Verwandte Algorithmen</h2></div>

<p>Seit 1986 werden auch (reduzierte geordnete) <a href="Bin%C3%A4res_Entscheidungsdiagramm" title="Binäres Entscheidungsdiagramm">binäre Entscheidungsbäume</a> zur <a href="SAT-Solver" class="mw-redirect" title="SAT-Solver">SAT-Lösung</a> verwendet.

</p><p>In den Jahren 1989–1990 wurde die Stålmarck-Methode zur Formelüberprüfung vorgestellt und patentiert. Sie hat einige Verwendung in industriellen Anwendungen gefunden.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup>

</p><p>DPLL wurde für das automatische Theorembeweisen für Fragmente der <a href="Logik_erster_Ordnung" class="mw-redirect" title="Logik erster Ordnung">Logik erster Ordnung</a> durch den DPLL(T)-Algorithmus erweitert.

</p><p>In den Jahren 2010 bis 2019 wurde an der Verbesserung des Algorithmus gearbeitet und bessere Strategien für die Auswahl der Verzweigungsliterale und neue Datenstrukturen gefunden, um den Algorithmus schneller zu machen, insbesondere den Teil der <i>unit propagation</i>. Die wichtigste Verbesserung war jedoch ein leistungsfähigerer Algorithmus, Conflict-Driven Clause Learning (CDCL), der ähnlich wie DPLL ist, aber nach dem Erreichen eines Konflikts die Ursachen (Zuweisungen an Variablen) des Konflikts „lernt“ und diese Informationen verwendet, um <i>nicht-chronologisches Backtracking</i> (auch bekannt als <i>Backjumping</i>) durchzuführen, um ein erneutes Erreichen desselben Konflikts zu vermeiden. Die meisten modernen <a href="SAT-Solver" class="mw-redirect" title="SAT-Solver">SAT-Solver</a> basieren auf dem CDCL-Framework (Stand 2019).<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Weiterführende_Literatur"><span id="Weiterf.C3.BChrende_Literatur"></span>Weiterführende Literatur</h2></div>

<ul><li>Malay Ganai, Aarti Gupta, Dr. Aarti Gupta: <cite class="lang" lang="en" dir="auto" style="font-style:italic">SAT-based scalable formal verification solutions</cite>. Springer, 2007, ISBN 978-0-387-69166-4, <span style="white-space:nowrap">S.<span style="display:inline-block;width:.2em"> </span>23–32</span> (englisch).<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:DPLL-Algorithmus&rft.au=Malay+Ganai%2C+Aarti+Gupta%2C+Dr.+Aarti+Gupta&rft.btitle=SAT-based+scalable+formal+verification+solutions&rft.date=2007&rft.genre=book&rft.isbn=9780387691664&rft.pages=23-32&rft.pub=Springer" style="display:none"> </span></li>

<li>Carla P. Gomes, Henry Kautz, Ashish Sabharwal, Bart Selman: <cite class="lang" lang="en" dir="auto" style="font-style:italic">Handbook of knowledge representation</cite>. Hrsg.: Frank Van Harmelen, Vladimir Lifschitz, Bruce Porter (= <cite class="lang" lang="en" dir="auto" style="font-style:italic">Foundations of Artificial Intelligence</cite>. <span style="white-space:nowrap">Band<span style="display:inline-block;width:.2em"> </span>3</span>). Elsevier, 2008, ISBN 978-0-444-52211-5, Satisfiability Solvers, <span style="white-space:nowrap">S.<span style="display:inline-block;width:.2em"> </span>89–134</span>, <a href="Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<span class="uri-handle" style="white-space:nowrap"><a rel="nofollow" class="external text" href="https://doi.org/10.1016/S1574-6526%2807%2903002-7">10.1016/S1574-6526(07)03002-7</a></span> (englisch).<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abookitem&rfr_id=info:sid/de.wikipedia.org:DPLL-Algorithmus&rft.atitle=Satisfiability+Solvers&rft.au=Carla+P.+Gomes%2C+Henry+Kautz%2C+Ashish+Sabharwal%2C+...&rft.btitle=Handbook+of+knowledge+representation&rft.date=2008&rft.doi=10.1016%2FS1574-6526%2807%2903002-7&rft.genre=bookitem&rft.isbn=9780444522115&rft.pages=89-134&rft.pub=Elsevier&rft.series=Foundations+of+Artificial+Intelligence" style="display:none"> </span></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Weblinks">Weblinks</h2></div>

<div class="sisterproject" style="margin:0.1em 0 0 0;"><div class="noresize noviewer" style="display:inline-block; line-height:10px; min-width:1.6em; text-align:center;" aria-hidden="true" role="presentation"><span class="mw-default-size" typeof="mw:File"><span title="Commons"></span></span></div><b><span class=""><a class="external text" href="https://commons.wikimedia.org/wiki/Category:Davis-Putnam-Logemann-Loveland_algorithm?uselang=de"><span lang="en">Commons</span>: DPLL-Algorithmus</a></span></b> – Sammlung von Bildern, Videos und Audiodateien</div>

<div class="mw-heading mw-heading2"><h2 id="Einzelnachweise">Einzelnachweise</h2></div>

<li id="cite_note-1"><span class="mw-cite-backlink"><a href="#cite_ref-1">↑</a></span> <span class="reference-text">Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: <cite style="font-style:italic">Abstract DPLL and Abstract DPLL Modulo Theories</cite>. In: <cite style="font-style:italic">Logic for Programming, Artificial Intelligence, and Reasoning</cite> (= <cite style="font-style:italic">Lecture Notes in Computer Science</cite>). Springer, Berlin, Heidelberg 2005, ISBN 3-540-32275-2, <span style="white-space:nowrap">S.<span style="display:inline-block;width:.2em"> </span>36–50</span>, <a href="Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<span class="uri-handle" style="white-space:nowrap"><a rel="nofollow" class="external text" href="https://doi.org/10.1007/978-3-540-32275-7_3">10.1007/978-3-540-32275-7_3</a></span> (<a rel="nofollow" class="external text" href="https://link.springer.com/chapter/10.1007/978-3-540-32275-7_3">springer.com</a> [abgerufen am 20. Januar 2024]).<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:DPLL-Algorithmus&rft.atitle=Abstract+DPLL+and+Abstract+DPLL+Modulo+Theories&rft.au=Robert+Nieuwenhuis%2C+Albert+Oliveras%2C+Cesare+Tinelli&rft.btitle=Logic+for+Programming%2C+Artificial+Intelligence%2C+and+Reasoning&rft.date=2005&rft.doi=10.1007%2F978-3-540-32275-7_3&rft.genre=book&rft.isbn=3540322752&rft.pages=36-50&rft.place=Berlin%2C+Heidelberg&rft.pub=Springer&rft.series=Lecture+Notes+in+Computer+Science" style="display:none"> </span></span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><a href="#cite_ref-2">↑</a></span> <span class="reference-text"><span class="cite"><a rel="nofollow" class="external text" href="http://www.princeton.edu/~chaff/zchaff.html"><i>Boolean Satisfiability Research Group at Princeton.</i></a><span class="Abrufdatum"> Abgerufen am 20. Januar 2024</span>.</span><span style="display: none;" class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rfr_id=info%3Asid%2Fde.wikipedia.org%3ADPLL-Algorithmus&rft.title=Boolean+Satisfiability+Research+Group+at+Princeton&rft.description=Boolean+Satisfiability+Research+Group+at+Princeton&rft.identifier=http%3A%2F%2Fwww.princeton.edu%2F%7Echaff%2Fzchaff.html"> </span></span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><a href="#cite_ref-3">↑</a></span> <span class="reference-text"><span class="cite"><a rel="nofollow" class="external text" href="http://minisat.se/"><i>MiniSat Page.</i></a><span class="Abrufdatum"> Abgerufen am 20. Januar 2024</span>.</span><span style="display: none;" class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rfr_id=info%3Asid%2Fde.wikipedia.org%3ADPLL-Algorithmus&rft.title=MiniSat+Page&rft.description=MiniSat+Page&rft.identifier=http%3A%2F%2Fminisat.se%2F"> </span></span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><a href="#cite_ref-4">↑</a></span> <span class="reference-text"><span class="cite"><a rel="nofollow" class="external text" href="http://www.satcompetition.org/"><i>SAT Competitions.</i></a><span class="Abrufdatum"> Abgerufen am 20. Januar 2024</span>.</span><span style="display: none;" class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rfr_id=info%3Asid%2Fde.wikipedia.org%3ADPLL-Algorithmus&rft.title=SAT+Competitions&rft.description=SAT+Competitions&rft.identifier=http%3A%2F%2Fwww.satcompetition.org%2F"> </span></span>

</li>

<li id="cite_note-5"><span class="mw-cite-backlink"><a href="#cite_ref-5">↑</a></span> <span class="reference-text">G. Stålmarck, M. Säflund: <cite class="lang" lang="en" dir="auto" style="font-style:italic">Modeling and Verifying Systems and Software in Propositional Logic</cite>. In: <cite class="lang" lang="en" dir="auto" style="font-style:italic">IFAC Proceedings Volumes</cite>. <span style="white-space:nowrap">Band<span style="display:inline-block;width:.2em"> </span>23</span>, <span style="white-space:nowrap">Nr.<span style="display:inline-block;width:.2em"> </span>6</span>, Oktober 1990, <span style="white-space:nowrap">S.<span style="display:inline-block;width:.2em"> </span>31–36</span>, <a href="Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<span class="uri-handle" style="white-space:nowrap"><a rel="nofollow" class="external text" href="https://doi.org/10.1016/S1474-6670%2817%2952173-4">10.1016/S1474-6670(17)52173-4</a></span> (englisch).<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rfr_id=info:sid/de.wikipedia.org:DPLL-Algorithmus&rft.atitle=Modeling+and+Verifying+Systems+and+Software+in+Propositional+Logic&rft.au=G.+St%C3%A5lmarck%2C+M.+S%C3%A4flund&rft.date=1990-10&rft.doi=10.1016%2FS1474-6670%2817%2952173-4&rft.genre=journal&rft.issue=6&rft.jtitle=IFAC+Proceedings+Volumes&rft.pages=31-36&rft.volume=23" style="display:none"> </span></span>

</li>

<li id="cite_note-6"><span class="mw-cite-backlink"><a href="#cite_ref-6">↑</a></span> <span class="reference-text">Sibylle Möhle, Armin Biere: <cite style="font-style:italic">Theory and Applications of Satisfiability Testing – SAT 2019</cite> (= <cite style="font-style:italic">Lecture Notes in Computer Science</cite>. <span style="white-space:nowrap">Band<span style="display:inline-block;width:.2em"> </span>11628</span>). 2019, ISBN 978-3-03024257-2, Backing Backtracking, <span style="white-space:nowrap">S.<span style="display:inline-block;width:.2em"> </span>250–266</span>, <a href="Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<span class="uri-handle" style="white-space:nowrap"><a rel="nofollow" class="external text" href="https://doi.org/10.1007/978-3-030-24258-9_18">10.1007/978-3-030-24258-9_18</a></span> (<a rel="nofollow" class="external text" href="http://fmv.jku.at/papers/MoehleBiere-SAT19.pdf">jku.at</a> [PDF]).<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abookitem&rfr_id=info:sid/de.wikipedia.org:DPLL-Algorithmus&rft.atitle=Backing+Backtracking&rft.au=Sibylle+M%C3%B6hle%2C+Armin+Biere&rft.btitle=Theory+and+Applications+of+Satisfiability+Testing+-+SAT+2019&rft.date=2019&rft.doi=10.1007%2F978-3-030-24258-9_18&rft.genre=bookitem&rft.isbn=9783030242572&rft.pages=250-266&rft.series=Lecture+Notes+in+Computer+Science" style="display:none"> </span></span>

</li>

</ol></div></div><div><div class="zim-footer">

Dieser Artikel wurde von <a class="external text" title="Zuletzt bearbeitet am 2025-09-18" href="https://de.wikipedia.org/wiki/?title=DPLL-Algorithmus&oldid=259842017">Wikipedia</a> herausgegeben. Der Text ist unter <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.de">Creative Commons Attribution-Share Alike 4.0</a> verfügbar, sofern nicht anders angegeben. Für die Mediendateien können zusätzliche Bedingungen gelten.

</div>

</div></div>

</div>

</main>

</div>

</body></html>